Life cycle of a program is in two phases:

Static

Anything that happens before running the program, i.e. compile time. E.g.

• static analysis
• parsing
• type checking
• lexing
• macros

Dynamic

Everything that happens when the program is run. (runtime) E.g.

• Program itself
• Side-effects (IO, exceptions)
• Memory management

---

Typing Judgements

%%🖋 Edit in Excalidraw%%

Environment/Context

Set of variables with type assignments e.g. $\gamma = \{x:t, y:\sigma\}$

Terms

A term is an expression which has been typed through a typing judgement. Anything else is a preterm. So a term is a well-typed preterm.

Binders

A binder is a language construct that closes over or binds variables e.g. $\forall$, $\exists$, let , $\sum$

Bound variables are variables that are bound or introduced by a binder.

A free variable is a variable that hasn’t been bound.

%%🖋 Edit in Excalidraw%% A closed expression is an expression with no free variables e.g. $\lambda t . t$ $\lambda y.yy$ An open expression is an expression with free variables e.g. $\lambda x.xy$ $lambda x.z$

$=_\alpha$ Equivalence/convertibility states that the name of a bound variable doesn’t matter. E.g. $\lambda x.x =_\alpha \lambda y.y.$ $\lambda a.ab =_\alpha \lambda x.xb$

A little language of numbers and strings

Syntax

Backus-Naur Form (BNF) syntactic chart is the form we will use to define the syntax.

Types - $\tau$

%%🖋 Edit in Excalidraw%% Abstract syntax - syntax of the term as it should appear in the Abstract Syntax Tree, i.e. how it’s represented for computation. Concrete syntax - User-friendly abbreviation of the abstract syntax.

Pre-terms - $e$

%%🖋 Edit in Excalidraw%%

Typing

%%🖋 Edit in Excalidraw%%

Cards

Q: What is the structure of a typing judgement? A:

Q: What does the context/environment (gamma) in a typing judgement hold? A: Sets of variables with their type assignments.

Q: What is a term? A: An expression which has been typed through a typing judgement. Anything else is a preterm.

Q: What is the difference between a closed/open expression? A: A closed expression has no free variables, an open expression has free variables.

Q: What is the symbol for saying that two expressions are equivalent? A: $=_\alpha$